Nuprl Lemma : function_functionality_wrt_equipollent_right 11,40

ABC:Type.  A ~ B   CA ~ CB 
latex


Definitionsx:A  B(x), x:AB(x), x:AB(x), Bij(A;B;f), P  Q, Type, x:AB(x),  A ~ B, Surj(A;B;f), Inj(A;B;f), P & Q, f o g, x.A(x), s = t, f(a), t  T, s ~ t,
Lemmascompose wf

origin